\begin{tabbing}
EKind\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type$_{\mbox{\scriptsize i}}$\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$Top
\\[0ex]$\times$${\it pred?}$:($E$$\rightarrow$($E$+Unit))
\\[0ex]$\times$${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id))
\\[0ex]$\times$EO\=rderAxioms\{i\}($E$;\+
\\[0ex]${\it pred?}$;
\\[0ex]${\it info}$)
\-\\[0ex]$\times$$T$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$${\it when}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc(${\it info}$;$e$),$x$))
\\[0ex]$\times$${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc(${\it info}$;$e$),$x$))
\\[0ex]$\times$(\=$\forall$$e$:$E$.\+
\\[0ex]$\neg$first(${\it pred?}$;$e$) $\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) $=$ ${\it after}$($x$,pred(${\it pred?}$;$e$)) $\in$ $T$(loc(${\it info}$;$e$),$x$)))
\-\\[0ex]$\times$Top
\-
\end{tabbing}